Natural-rule System
次の生成規則
$ \land\text{前}:$ A \land B \implies A
$ \land\text{後}: $ A,B \implies A \land B
$ \lor{後}:$ A \implies A \lor Bまたは$ A \implies B \lor A
$ \to\text{前}(モーダス・ポネンス): $ A \to B, A \implies B $ \lnot\text{前}: $ A, \lnot A \implies \bot
$ \bot: $ \bot \implies X
二重否定: $ \lnot\lnot A \implies A 証明構造に関する規則（$ \Gammaは有限個の論証とする）
$ \to\text{後}:$ A, \Gamma \to B \implies \Gamma \to (A \to B)
$ \lnot\text{後}: $ A, \Gamma \to \bot \implies \Gamma \to \lnot A
$ \lor{前}: $ (A,\Gamma_1 \to C), (B,\Gamma_2 \to C) \implies (\Gamma_1, \Gamma_2) \to (A \lor B \to C)